(* It's crucial that this file does NOT end with a newline. This should give an
   error message but shouldn't get into an infinite loop! *)
0 0;